Nuprl Lemma : atom-deq-aux
0,22
postcript
pdf
a
,
b
:Atom.
a
=
b
a
=
b
Atom
latex
Definitions
t
T
,
Prop
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
=
y
Atom
,
b
,
x
.
t
(
x
)
Lemmas
all
functionality
wrt
iff
,
iff
functionality
wrt
iff
,
assert
of
eq
atom
,
iff
wf
,
assert
wf
,
eq
atom
wf
origin
a, b:Atom. a = b 
a=
b
Atom a, b:Atom. a = b a=bAtom T
Q Q Qx:A. B(x)yAtom
b
x. t(x)